Inference at * 1 0 1 3 1 
Iof proof for Lemma nat ind:



1. P : {k}
2. P(0)
3. i:. P(i - 1)  P(i)
4. j : 
5. 0 < j
6. ((j - 1)  0 )  P(j - 1)
7. j  0 
  P(j) 

latex

 by ((Thin (-1)) 
CollapseTHEN (D (-1))) 

latex

C1: .....antecedent..... NILNIL

C1: 5. 0 < j
C1:   (j - 1)  0 
C2: 

C2: 6. P(j - 1)
C2:   P(j)
C.

Definitions

i  j , a < b, , n - m, , x:A. B(x), #$n, x(s), , , x:AB(x), P  Q